Skip to content

feat(Tactic/Positivity): cover Finset.sum_pos' with the Finset.sum extension - #43613

Open
YaelDillies wants to merge 8 commits into
leanprover-community:masterfrom
YaelDillies:positivity_finset_sum_pos
Open

feat(Tactic/Positivity): cover Finset.sum_pos' with the Finset.sum extension#43613
YaelDillies wants to merge 8 commits into
leanprover-community:masterfrom
YaelDillies:positivity_finset_sum_pos

Conversation

@YaelDillies

@YaelDillies YaelDillies commented Sep 9, 2026

Copy link
Copy Markdown
Contributor

To prove 0 < ∑ a ∈ s, f a, the positivity extension now also searches through assumptions of the form a ∈ s and for each of them tries to prove 0 < f a.

Will be used in convexity theory.

Generated by Claude Opus

Assisted-by: Claude Opus 5

Open in Gitpod

@YaelDillies
feat(Tactic/Positivity): cover Finset.sum_pos' with the `Finset.sum…
8fa82e8 
…` extension

To prove `0 < ∑ a ∈ s, f a`, the `positivity` extension now also searches through assumptions of the form `a ∈ s` and for each of them tries to prove `0 < f a`.

Will be used in convexity theory.

Generated by Claude Opus

Assisted-by: Claude Opus 5
@github-actions

github-actions Bot commented Sep 9, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary e4d0a9f376

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff (regex)

+ instantiateMVarsQ'

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit e4d0a9f).

  • +1 new declarations
  • −0 removed declarations
+Qq.instantiateMVarsQ'

No changes to strong technical debt.
No changes to weak technical debt.

Current commit e4d0a9f376
Reference commit 97ac4d32b0

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions Bot added the t-meta Tactics, attributes or user commands label Sep 9, 2026
eric-wieser
eric-wieser reviewed Sep 9, 2026
View reviewed changes
Comment thread Mathlib/Tactic/Positivity/Finset.lean Outdated
@grunweg grunweg added the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Sep 9, 2026
@YaelDillies YaelDillies mentioned this pull request Sep 9, 2026
Open
3 tasks
@YaelDillies YaelDillies added the LLM-generated PRs with substantial input from LLMs - review accordingly label Sep 9, 2026
@YaelDillies YaelDillies removed the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Sep 9, 2026
eric-wieser
eric-wieser reviewed Sep 9, 2026
View reviewed changes
Comment thread Mathlib/Tactic/Positivity/Finset.lean Outdated
eric-wieser
eric-wieser reviewed Sep 9, 2026
View reviewed changes
Comment thread Mathlib/Tactic/Positivity/Finset.lean Outdated
eric-wieser
eric-wieser reviewed Sep 9, 2026
View reviewed changes
Comment thread Mathlib/Tactic/Positivity/Finset.lean Outdated
eric-wieser
eric-wieser reviewed Sep 9, 2026
View reviewed changes
Comment thread Mathlib/Tactic/Positivity/Finset.lean
eric-wieser
eric-wieser reviewed Sep 9, 2026
View reviewed changes

@eric-wieser eric-wieser left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

maintainer delegate

This looks like a pretty good idea to me

@github-actions

github-actions Bot commented Sep 9, 2026

Copy link
Copy Markdown

🚀 Pull request has been placed on the maintainer queue by eric-wieser.

@mathlib-triage mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 9, 2026
eric-wieser
eric-wieser reviewed Sep 9, 2026
View reviewed changes
Comment thread Mathlib/Tactic/Positivity/Finset.lean Outdated
@YaelDillies @eric-wieser
withReducible
e4d0a9f 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

Assignees

No one assigned

Labels

LLM-generated PRs with substantial input from LLMs - review accordingly maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@YaelDillies @eric-wieser @grunweg